Theorem 3impia 1117

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)

Hypothesis

Ref	Expression
3impia.1	⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Assertion

Ref	Expression
3impia	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	expimpd 453	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	3impib 1116	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088

This theorem is referenced by:  mopick2  2631  ceqsalt  3468  3gencl  3478  vtoclgft  3505  vtoclegft  3541  rspc6v  3596  mob2  3672  moi  3675  reupick3  4278  disjne  4403  elpr2elpr  4819  disji2  5073  disji  5074  tz7.2  5597  sofld  6131  ordintdif  6353  funopg  6511  fvun1  6908  fvopab6  6958  fveqressseq  7007  fvcofneq  7021  fprg  7083  isores3  7264  ovmpt4g  7488  ovmpos  7489  ov2gf  7490  ofrval  7617  sorpssuni  7660  sorpssint  7661  poxp  8053  poseq  8083  suppss2  8125  frrlem12  8222  smoel  8275  smoord  8280  smogt  8282  oaass  8471  oewordi  8501  oeoalem  8506  oeoelem  8508  nnawordi  8531  nnaass  8532  naddssim  8595  qsel  8715  xpdom3  8983  onsdominel  9034  mapdom3  9057  sdomdomtrfi  9105  domsdomtrfi  9106  php  9111  onomeneq  9118  fisseneq  9142  fodomfir  9207  cantnflem1  9574  ttrclss  9605  cfslbn  10150  cfsmolem  10153  cfcoflem  10155  infpssrlem4  10189  fin23lem7  10199  fin23lem25  10207  isf34lem7  10262  hsmexlem2  10310  axcc3  10321  axdc4lem  10338  tskss  10641  gruss  10679  gruurn  10681  gruiun  10682  gruel  10686  gruen  10695  grudomon  10700  grothac  10713  axpre-sup  11052  axsup  11180  addn0nid  11529  letrp1  11957  p1le  11958  lemul1a  11967  infrelb  12099  zextle  12538  zextlt  12539  btwnnz  12541  gtndiv  12542  uzind2  12558  fzind  12563  eluzsubOLD  12760  zsupss  12827  xrltne  13054  lemaxle  13086  qbtwnre  13090  qbtwnxr  13091  xlemul1a  13179  icogelb  13288  iccleub  13293  iccsplit  13377  uzsubsubfz  13438  elfz0fzfz0  13525  difelfznle  13534  fvffz0  13538  elfzo0le  13595  fzonmapblen  13600  fzofzim  13601  ceile  13745  modadd1  13804  muladdmodid  13809  modmul1  13823  modirr  13841  fsuppmapnn0fiub0  13892  expcl2lem  13972  expclzlem  13982  expnegz  13995  leexp2r  14073  bcval4  14206  bccmpl  14208  hashbnd  14235  hashunsnggt  14293  hashgt23el  14323  hashfundm  14341  elovmpowrd  14457  ccatval2  14477  ccatrcl1  14494  wrdl1s1  14514  ccat2s1fvw  14538  swrdsb0eq  14563  swrdccatin1  14624  pfxccatpfx2  14636  repswswrd  14683  cshwcsh2id  14727  absexpz  15204  climbdd  15571  iseraltlem2  15582  binomfallfac  15940  dvdsle  16213  divalgb  16307  ndvdssub  16312  dvdsgcd  16447  dfgcd2  16449  rplpwr  16461  nn0rppwr  16464  nn0expgcd  16467  lcmgcdlem  16509  lcmfunsn  16547  coprmdvds1  16555  qredeq  16560  2mulprm  16596  prmdvdsexpr  16620  nnnn0modprm0  16710  prm23ge5  16719  pcexp  16763  difsqpwdvds  16791  prmpwdvds  16808  ramcl  16933  cshwshashlem3  17001  cshwrepswhash1  17006  elrestr  17324  mreintcl  17489  mremre  17498  mrieqv2d  17537  initoeu2lem1  17913  funcestrcsetclem9  18046  funcsetcestrclem9  18061  prstr  18197  drsdirfi  18203  latnlej  18354  latnlej2  18357  acsdrsel  18441  acsdrscl  18444  mrelatglb  18458  mrelatlub  18460  isnmgm  18544  grpasscan1  18906  grpinvnz  18915  mulgneg2  19013  gsmsymgrfix  19333  f1omvdco2  19353  symggen  19375  odcl2  19470  odhash3  19481  lsmss1  19570  lsmss2  19572  efgred  19653  efgcpbl  19661  ablfacrp  19973  ablfac1eu  19980  ablfaclem3  19994  omndadd  20033  ogrpaddlt  20043  dvdsrmul1  20280  dvdsunit  20290  irredmul  20340  c0snmgmhm  20373  lmodlema  20791  psgnodpmr  21520  phlssphl  21589  lindsss  21754  lindfmm  21757  ply1scln0  22199  dmatelnd  22404  mdetdiaglem  22506  mdet0  22514  mdetunilem7  22526  slesolinv  22588  cramerimplem3  22593  cpmatpmat  22618  m2cpminvid2lem  22662  chfacfscmul0  22766  chfacfpmmul0  22770  riinopn  22816  clsndisj  22983  cnpf2  23158  hausnei2  23261  cmpcov  23297  cmpfii  23317  unconn  23337  t1connperf  23344  nrmr0reg  23657  fbfinnfr  23749  filuni  23793  alexsubALT  23959  tmdgsum  24003  cuspcvg  24208  mopni  24400  isngp4  24520  metdsre  24762  iimulcl  24853  phtpc01  24915  clmmulg  25021  cfilucfil4  25241  bcthlem5  25248  bcth  25249  bcth3  25251  itg1le  25634  itg2le  25660  bddmulibl  25760  bddiblnc  25763  dvnres  25853  cpnord  25857  dvnfre  25876  deg1ge  26023  dgr1term  26185  aaliou3lem2  26271  sincosq1lem  26426  cxpge0  26612  cxpmul2  26618  logrec  26693  logbgcd1irr  26724  sqfpc  27067  bcmono  27208  gausslemma2dlem1a  27296  gausslemma2dlem2  27298  gausslemma2dlem4  27300  2lgsoddprmlem3  27345  pntrmax  27495  qabvexp  27557  ostth2lem2  27565  nosepon  27597  nolesgn2o  27603  nogesgn1o  27605  nosepnelem  27611  nosepne  27612  nosepdmlem  27615  nosepdm  27616  nodenselem8  27623  noresle  27629  noetasuplem4  27668  noetainflem4  27672  scutbdaylt  27752  eqscut3  27758  addsuniflem  27937  ssltmul1  28079  precsexlem6  28143  precsexlem7  28144  precsexlem11  28148  sltonold  28191  onnolt  28196  n0sfincut  28275  expadds  28351  ax5seglem4  28903  axeuclidlem  28933  uhgredgrnv  29101  usgredg4  29188  nbuhgr2vtx1edgblem  29322  vtxduhgr0e  29450  vtxduhgr0nedg  29464  rusgrpropnb  29555  uspgr2wlkeqi  29619  redwlklem  29641  lfgrwlkprop  29657  2pthnloop  29702  spthonepeq  29723  pthdlem2lem  29738  crctcshwlkn0lem3  29783  crctcshwlkn0lem5  29785  crctcshwlkn0lem7  29787  crctcshwlkn0  29792  wlkiswwlks1  29838  wlkiswwlks2  29846  wlkiswwlksupgr2  29848  wwlksnext  29864  wwlksnextproplem2  29881  wspthsnonn0vne  29888  2pthon3v  29914  rusgrnumwwlk  29946  erclwwlkeqlen  29989  erclwwlksym  29991  erclwwlktr  29992  erclwwlkneqlen  30038  erclwwlknsym  30040  erclwwlkntr  30041  uhgr3cyclex  30152  upgreupthseg  30179  eupth2lem3lem4  30201  eucrctshift  30213  4cycl2vnunb  30260  nvs  30633  nvtri  30640  nmlno0  30765  nmlnoubi  30766  ubth  30843  hlipgt0  30884  ocnel  31268  elspansn2  31537  elspansn3  31542  normcan  31546  pjoml2  31581  lecm  31587  osum  31615  nmbdfnlb  32020  leopmul  32104  hstpyth  32199  cvnbtwn  32256  ssmd1  32281  ssmd2  32282  ssdmd1  32283  ssdmd2  32284  cvmd  32306  cvdmd  32307  superpos  32324  disji2f  32547  disjif  32548  disjif2  32551  preiman0  32681  padct  32691  ffs2  32700  bcm1n  32767  sgn3da  32807  s2f1  32916  archiabl  33157  slmdlema  33162  lbslsat  33619  eulerpartlemb  34371  fisshasheq  35127  cvmsdisj  35282  cvmlift2lem12  35326  satfrel  35379  satfrnmapom  35382  fmlasuc  35398  satffun  35421  satef  35428  sategoelfv  35432  lineintmo  36170  nn0prpwlem  36335  nn0prpw  36336  neibastop2lem  36373  lindsadd  37632  areacirc  37732  incsequz  37767  mettrifi  37776  ismtybnd  37826  heiborlem1  37830  rngoisocnv  38000  risci  38006  eqvrelqsel  38632  lfl1  39088  lkrlsp2  39121  omlfh3N  39277  cvrnbtwn  39289  cvrnbtwn2  39293  cvrnbtwn4  39297  cvlexch3  39350  cvlexch4N  39351  cvlatexchb1  39352  2llnne2N  39426  atcvrj0  39446  cvrat2  39447  ps-1  39495  3atlem5  39505  islln2a  39535  lplnriaN  39568  lplnribN  39569  llncvrlpln2  39575  lplncvrlvol2  39633  psubatN  39773  pmapglb2N  39789  pmapglb2xN  39790  2llnma1b  39804  paddasslem17  39854  pmod2iN  39867  pmodl42N  39869  hlmod1i  39874  atmod1i1  39875  atmod1i2  39877  llnmod1i2  39878  pclcmpatN  39919  osumcllem8N  39981  pexmidlem3N  39990  pl42lem4N  40000  4atexlem7  40093  ltrnnid  40154  cdlemc4  40212  cdleme32a  40459  cdlemeg46gfre  40550  cdlemf2  40580  cdlemg4c  40630  trlcoat  40741  tendovalco  40783  tendoeq2  40792  cdlemk36  40931  diael  41061  diatrl  41062  dicelval1stN  41206  dicelval2nd  41207  dihlspsnat  41351  dochkr1  41496  lcfrlem9  41568  mapdh8e  41802  hdmapval0  41851  hgmapval0  41910  nnadddir  42282  dvdsexpnn0  42346  incssnn0  42723  pell14qrexpcl  42879  pell14qrgap  42887  congadd  42978  acongsym  42988  acongtr  42990  dvdsacongtr  42996  jm2.19lem3  43003  jm2.19lem4  43004  jm2.26lem3  43013  onexlimgt  43255  nadd2rabex  43398  ismnushort  44313  bi13impia  44501  3impcombi  44828  ioogtlb  45514  iocgtlb  45521  iocleub  45522  icoltub  45527  iooltub  45529  limclner  45668  limsupre3lem  45749  climuzlem  45760  fsupdm  46859  finfdm  46863  elfzelfzlble  47331  subsubelfzo0  47336  m1modnep2mod  47362  m1modmmod  47368  modlt0b  47373  mod2addne  47374  iccpartigtl  47433  sqrtpwpw2p  47548  fmtnoprmfac1lem  47574  fmtno4prmfac  47582  evenltle  47727  even3prm2  47729  wtgoldbnnsum4prm  47812  bgoldbnnsum3prm  47814  bgoldbtbndlem1  47815  bgoldbtbndlem3  47817  bgoldbtbndlem4  47818  bgoldbtbnd  47819  uhgrimisgrgriclem  47940  isubgr3stgrlem7  47982  clnbgr3stgrgrlic  48030  gpgedg2iv  48077  pgnbgreunbgrlem3  48128  pgnbgreunbgrlem6  48134  upgrwlkupwlk  48150  funcringcsetcALTV2lem9  48308  funcringcsetclem9ALTV  48331  lincscmcl  48443  lindslinindimp2lem4  48472  lincresunit2  48489  lincresunit3  48492  elfzolborelfzop1  48530  rege1logbzge0  48570  fllog2  48579  dignn0ldlem  48613  rrx2pnecoorneor  48726  rrx2plord2  48733  rrx2linest  48753  ipolub  48998  ipoglb  49001