Theorem 3impia 1118

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 1117	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

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

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 1089

This theorem is referenced by:  mopick2  2638  ceqsalt  3464  3gencl  3474  vtoclgft  3498  rspc6v  3586  mob2  3662  moi  3665  reupick3  4271  disjne  4396  elpr2elpr  4813  disji2  5070  disji  5071  tz7.2  5607  sofld  6145  ordintdif  6368  funopg  6526  fvun1  6925  fvopab6  6976  fveqressseq  7025  fvcofneq  7039  fprg  7102  isores3  7283  ovmpt4g  7507  ovmpos  7508  ov2gf  7509  ofrval  7636  sorpssuni  7679  sorpssint  7680  poxp  8071  poseq  8101  suppss2  8143  frrlem12  8240  smoel  8293  smoord  8298  smogt  8300  oaass  8489  oewordi  8520  oeoalem  8525  oeoelem  8527  nnawordi  8550  nnaass  8551  naddssim  8614  qsel  8736  xpdom3  9006  onsdominel  9057  mapdom3  9080  sdomdomtrfi  9128  domsdomtrfi  9129  php  9134  onomeneq  9141  fisseneq  9166  fodomfir  9231  cantnflem1  9601  ttrclss  9632  cfslbn  10180  cfsmolem  10183  cfcoflem  10185  infpssrlem4  10219  fin23lem7  10229  fin23lem25  10237  isf34lem7  10292  hsmexlem2  10340  axcc3  10351  axdc4lem  10368  tskss  10672  gruss  10710  gruurn  10712  gruiun  10713  gruel  10717  gruen  10726  grudomon  10731  grothac  10744  axpre-sup  11083  axsup  11212  addn0nid  11561  letrp1  11990  p1le  11991  lemul1a  12000  infrelb  12132  nnadddir  12224  zextle  12593  zextlt  12594  btwnnz  12596  gtndiv  12597  uzind2  12613  fzind  12618  zsupss  12878  xrltne  13105  lemaxle  13138  qbtwnre  13142  qbtwnxr  13143  xlemul1a  13231  icogelb  13340  iccleub  13345  iccsplit  13429  uzsubsubfz  13491  elfz0fzfz0  13578  difelfznle  13587  fvffz0  13591  elfzo0le  13649  fzonmapblen  13654  fzofzim  13655  ceile  13799  modadd1  13858  muladdmodid  13863  modmul1  13877  modirr  13895  fsuppmapnn0fiub0  13946  expcl2lem  14026  expclzlem  14036  expnegz  14049  leexp2r  14127  bcval4  14260  bccmpl  14262  hashbnd  14289  hashunsnggt  14347  hashgt23el  14377  hashfundm  14395  elovmpowrd  14511  ccatval2  14531  ccatrcl1  14548  wrdl1s1  14568  ccat2s1fvw  14592  swrdsb0eq  14617  swrdccatin1  14678  pfxccatpfx2  14690  repswswrd  14737  cshwcsh2id  14781  absexpz  15258  climbdd  15625  iseraltlem2  15636  binomfallfac  15997  dvdsle  16270  divalgb  16364  ndvdssub  16369  dvdsgcd  16504  dfgcd2  16506  rplpwr  16518  nn0rppwr  16521  nn0expgcd  16524  lcmgcdlem  16566  lcmfunsn  16604  coprmdvds1  16612  qredeq  16617  2mulprm  16653  prmdvdsexpr  16678  nnnn0modprm0  16768  prm23ge5  16777  pcexp  16821  difsqpwdvds  16849  prmpwdvds  16866  ramcl  16991  cshwshashlem3  17059  cshwrepswhash1  17064  elrestr  17382  mreintcl  17548  mremre  17557  mrieqv2d  17596  initoeu2lem1  17972  funcestrcsetclem9  18105  funcsetcestrclem9  18120  prstr  18256  drsdirfi  18262  latnlej  18413  latnlej2  18416  acsdrsel  18500  acsdrscl  18503  mrelatglb  18517  mrelatlub  18519  isnmgm  18603  grpasscan1  18968  grpinvnz  18977  mulgneg2  19075  gsmsymgrfix  19394  f1omvdco2  19414  symggen  19436  odcl2  19531  odhash3  19542  lsmss1  19631  lsmss2  19633  efgred  19714  efgcpbl  19722  ablfacrp  20034  ablfac1eu  20041  ablfaclem3  20055  omndadd  20094  ogrpaddlt  20104  dvdsrmul1  20340  dvdsunit  20350  irredmul  20400  c0snmgmhm  20433  lmodlema  20851  psgnodpmr  21580  phlssphl  21649  lindsss  21814  lindfmm  21817  ply1scln0  22266  dmatelnd  22471  mdetdiaglem  22573  mdet0  22581  mdetunilem7  22593  slesolinv  22655  cramerimplem3  22660  cpmatpmat  22685  m2cpminvid2lem  22729  chfacfscmul0  22833  chfacfpmmul0  22837  riinopn  22883  clsndisj  23050  cnpf2  23225  hausnei2  23328  cmpcov  23364  cmpfii  23384  unconn  23404  t1connperf  23411  nrmr0reg  23724  fbfinnfr  23816  filuni  23860  alexsubALT  24026  tmdgsum  24070  cuspcvg  24275  mopni  24467  isngp4  24587  metdsre  24829  iimulcl  24914  phtpc01  24973  clmmulg  25078  cfilucfil4  25298  bcthlem5  25305  bcth  25306  bcth3  25308  itg1le  25690  itg2le  25716  bddmulibl  25816  bddiblnc  25819  dvnres  25908  cpnord  25912  dvnfre  25929  deg1ge  26073  dgr1term  26235  aaliou3lem2  26320  sincosq1lem  26474  cxpge0  26660  cxpmul2  26666  logrec  26740  logbgcd1irr  26771  sqfpc  27114  bcmono  27254  gausslemma2dlem1a  27342  gausslemma2dlem2  27344  gausslemma2dlem4  27346  2lgsoddprmlem3  27391  pntrmax  27541  qabvexp  27603  ostth2lem2  27611  nosepon  27643  nolesgn2o  27649  nogesgn1o  27651  nosepnelem  27657  nosepne  27658  nosepdmlem  27661  nosepdm  27662  nodenselem8  27669  noresle  27675  noetasuplem4  27714  noetainflem4  27718  cutbdaylt  27804  eqcuts3  27810  addsuniflem  28007  sltmuls1  28153  precsexlem6  28218  precsexlem7  28219  precsexlem11  28223  ltonold  28267  onnolt  28272  n0fincut  28361  oldfib  28383  expadds  28441  ax5seglem4  29015  axeuclidlem  29045  uhgredgrnv  29213  usgredg4  29300  nbuhgr2vtx1edgblem  29434  vtxduhgr0e  29562  vtxduhgr0nedg  29576  rusgrpropnb  29667  uspgr2wlkeqi  29731  redwlklem  29753  lfgrwlkprop  29769  2pthnloop  29814  spthonepeq  29835  pthdlem2lem  29850  crctcshwlkn0lem3  29895  crctcshwlkn0lem5  29897  crctcshwlkn0lem7  29899  crctcshwlkn0  29904  wlkiswwlks1  29950  wlkiswwlks2  29958  wlkiswwlksupgr2  29960  wwlksnext  29976  wwlksnextproplem2  29993  wspthsnonn0vne  30000  2pthon3v  30026  rusgrnumwwlk  30061  erclwwlkeqlen  30104  erclwwlksym  30106  erclwwlktr  30107  erclwwlkneqlen  30153  erclwwlknsym  30155  erclwwlkntr  30156  uhgr3cyclex  30267  upgreupthseg  30294  eupth2lem3lem4  30316  eucrctshift  30328  4cycl2vnunb  30375  nvs  30749  nvtri  30756  nmlno0  30881  nmlnoubi  30882  ubth  30959  hlipgt0  31000  ocnel  31384  elspansn2  31653  elspansn3  31658  normcan  31662  pjoml2  31697  lecm  31703  osum  31731  nmbdfnlb  32136  leopmul  32220  hstpyth  32315  cvnbtwn  32372  ssmd1  32397  ssmd2  32398  ssdmd1  32399  ssdmd2  32400  cvmd  32422  cvdmd  32423  superpos  32440  disji2f  32662  disjif  32663  disjif2  32666  preiman0  32798  padct  32806  ffs2  32815  bcm1n  32883  sgn3da  32922  s2f1  33020  archiabl  33274  slmdlema  33279  lbslsat  33776  eulerpartlemb  34528  fisshasheq  35313  cvmsdisj  35468  cvmlift2lem12  35512  satfrel  35565  satfrnmapom  35568  fmlasuc  35584  satffun  35607  satef  35614  sategoelfv  35618  lineintmo  36355  nn0prpwlem  36520  nn0prpw  36521  neibastop2lem  36558  tr0elw  36682  lindsadd  37948  areacirc  38048  incsequz  38083  mettrifi  38092  ismtybnd  38142  heiborlem1  38146  rngoisocnv  38316  risci  38322  eqvrelqsel  39035  lfl1  39530  lkrlsp2  39563  omlfh3N  39719  cvrnbtwn  39731  cvrnbtwn2  39735  cvrnbtwn4  39739  cvlexch3  39792  cvlexch4N  39793  cvlatexchb1  39794  2llnne2N  39868  atcvrj0  39888  cvrat2  39889  ps-1  39937  3atlem5  39947  islln2a  39977  lplnriaN  40010  lplnribN  40011  llncvrlpln2  40017  lplncvrlvol2  40075  psubatN  40215  pmapglb2N  40231  pmapglb2xN  40232  2llnma1b  40246  paddasslem17  40296  pmod2iN  40309  pmodl42N  40311  hlmod1i  40316  atmod1i1  40317  atmod1i2  40319  llnmod1i2  40320  pclcmpatN  40361  osumcllem8N  40423  pexmidlem3N  40432  pl42lem4N  40442  4atexlem7  40535  ltrnnid  40596  cdlemc4  40654  cdleme32a  40901  cdlemeg46gfre  40992  cdlemf2  41022  cdlemg4c  41072  trlcoat  41183  tendovalco  41225  tendoeq2  41234  cdlemk36  41373  diael  41503  diatrl  41504  dicelval1stN  41648  dicelval2nd  41649  dihlspsnat  41793  dochkr1  41938  lcfrlem9  42010  mapdh8e  42244  hdmapval0  42293  hgmapval0  42352  dvdsexpnn0  42780  incssnn0  43157  pell14qrexpcl  43313  pell14qrgap  43321  congadd  43412  acongsym  43422  acongtr  43424  dvdsacongtr  43430  jm2.19lem3  43437  jm2.19lem4  43438  jm2.26lem3  43447  onexlimgt  43689  nadd2rabex  43832  ismnushort  44746  bi13impia  44934  3impcombi  45261  ioogtlb  45943  iocgtlb  45950  iocleub  45951  icoltub  45956  iooltub  45958  limclner  46097  limsupre3lem  46178  climuzlem  46189  fsupdm  47288  finfdm  47292  elfzelfzlble  47781  subsubelfzo0  47787  m1modnep2mod  47818  m1modmmod  47824  modlt0b  47829  mod2addne  47830  iccpartigtl  47895  sqrtpwpw2p  48013  fmtnoprmfac1lem  48039  fmtno4prmfac  48047  evenltle  48205  even3prm2  48207  wtgoldbnnsum4prm  48290  bgoldbnnsum3prm  48292  bgoldbtbndlem1  48293  bgoldbtbndlem3  48295  bgoldbtbndlem4  48296  bgoldbtbnd  48297  uhgrimisgrgriclem  48418  isubgr3stgrlem7  48460  clnbgr3stgrgrlic  48508  gpgedg2iv  48555  pgnbgreunbgrlem3  48606  pgnbgreunbgrlem6  48612  upgrwlkupwlk  48628  funcringcsetcALTV2lem9  48786  funcringcsetclem9ALTV  48809  lincscmcl  48920  lindslinindimp2lem4  48949  lincresunit2  48966  lincresunit3  48969  elfzolborelfzop1  49007  rege1logbzge0  49047  fllog2  49056  dignn0ldlem  49090  rrx2pnecoorneor  49203  rrx2plord2  49210  rrx2linest  49230  ipolub  49475  ipoglb  49478