Theorem 3impia 1097

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 446	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	3impib 1096	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 387   ∧ w3a 1068

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 199  df-an 388  df-3an 1070

This theorem is referenced by:  mopick2  2663  3gencl  3451  vtoclgft  3468  mob2  3616  moi  3619  reupick3  4170  disjne  4281  elpr2elpr  4667  disji2  4907  disji  4908  tz7.2  5384  sofld  5878  ordintdif  6072  funopg  6216  fvun1  6576  fvopab6  6620  fveqressseq  6666  fvcofneq  6678  fprg  6734  2f1fvneq  6837  isores3  6905  ovmpt4g  7107  ovmpos  7108  ov2gf  7109  ofrval  7231  sorpssuni  7270  sorpssint  7271  poxp  7620  suppss2  7660  smoel  7794  smoord  7799  smogt  7801  oaass  7980  oewordi  8010  oeoalem  8015  oeoelem  8017  nnawordi  8040  nnaass  8041  qsel  8168  xpdom3  8403  onsdominel  8454  mapdom3  8477  fisseneq  8516  cantnflem1  8938  cfslbn  9479  cfsmolem  9482  cfcoflem  9484  infpssrlem4  9518  fin23lem7  9528  fin23lem25  9536  isf34lem7  9591  hsmexlem2  9639  axcc3  9650  axdc4lem  9667  tskss  9970  gruss  10008  gruurn  10010  gruiun  10011  gruel  10015  gruen  10024  grudomon  10029  grothac  10042  axpre-sup  10381  axsup  10508  addn0nid  10853  letrp1  11277  p1le  11278  lemul1a  11287  infrelb  11419  zextle  11861  zextlt  11862  btwnnz  11864  gtndiv  11865  uzind2  11881  fzind  11886  eluzsub  12081  zsupss  12144  xrltne  12366  lemaxle  12398  qbtwnre  12402  qbtwnxr  12403  xlemul1a  12490  icogelb  12597  iccleub  12601  iccsplit  12680  uzsubsubfz  12738  elfz0fzfz0  12821  difelfznle  12830  fvffz0  12834  elfzo0le  12889  fzonmapblen  12891  fzofzim  12892  ceile  13025  modadd1  13084  muladdmodid  13087  modmul1  13100  modirr  13118  fsuppmapnn0fiub0  13169  expcl2lem  13249  expclzlem  13261  expnegz  13271  leexp2r  13346  bcval4  13475  bccmpl  13477  hashbnd  13504  elovmpowrd  13711  ccatval2  13731  ccatrcl1  13747  wrdl1s1  13767  ccat2s1fvw  13791  swrdsb0eq  13830  swrdccatin1  13914  pfxccatpfx2  13931  repswswrd  13993  cshwcsh2id  14042  pfx2  14161  absexpz  14516  climbdd  14879  iseraltlem2  14890  binomfallfac  15245  dvdsle  15510  divalgb  15605  ndvdssub  15610  dvdsgcd  15738  dfgcd2  15740  rplpwr  15753  lcmgcdlem  15796  lcmfunsn  15834  coprmdvds1  15842  qredeq  15847  2mulprm  15883  prmdvdsexpr  15907  nnnn0modprm0  15989  prm23ge5  15998  pcexp  16042  difsqpwdvds  16069  prmpwdvds  16086  ramcl  16211  cshwshashlem3  16277  cshwrepswhash1  16282  elrestr  16548  xpscfv  16681  mreintcl  16714  mremre  16723  mrieqv2d  16758  initoeu2lem1  17122  funcestrcsetclem9  17246  funcsetcestrclem9  17261  prstr  17391  drsdirfi  17396  latnlej  17526  latnlej2  17529  acsdrsel  17625  acsdrscl  17628  mrelatglb  17642  mrelatlub  17644  isnmgm  17704  grpasscan1  17939  grpinvnz  17947  mulgneg2  18035  gsmsymgrfix  18307  f1omvdco2  18327  symggen  18349  odcl2  18443  odhash3  18452  lsmss1  18540  lsmss2  18542  efgred  18624  efgcpbl  18632  ablfacrp  18928  ablfac1eu  18935  ablfaclem3  18949  dvdsrmul1  19116  dvdsunit  19126  irredmul  19172  lmodlema  19351  ply1scln0  20152  psgnodpmr  20426  phlssphl  20495  lindsss  20660  lindfmm  20663  dmatelnd  20799  mdetdiaglem  20901  mdet0  20909  mdetunilem7  20921  slesolinv  20983  cramerimplem3  20988  cpmatpmat  21012  m2cpminvid2lem  21056  chfacfscmul0  21160  chfacfpmmul0  21164  riinopn  21210  clsndisj  21377  cnpf2  21552  hausnei2  21655  cmpcov  21691  cmpfii  21711  unconn  21731  t1connperf  21738  nrmr0reg  22051  fbfinnfr  22143  filuni  22187  alexsubALT  22353  tmdgsum  22397  cuspcvg  22603  mopni  22795  isngp4  22914  metdsre  23154  iimulcl  23234  phtpc01  23293  clmmulg  23398  cfilucfil4  23617  bcthlem5  23624  bcth  23625  bcth3  23627  itg1le  24007  itg2le  24033  bddmulibl  24132  dvnres  24221  cpnord  24225  dvnfre  24242  deg1ge  24385  dgr1term  24543  aaliou3lem2  24625  sincosq1lem  24776  cxpge0  24957  cxpmul2  24963  logrec  25032  logbgcd1irr  25063  sqfpc  25406  bcmono  25545  gausslemma2dlem1a  25633  gausslemma2dlem2  25635  gausslemma2dlem4  25637  2lgsoddprmlem3  25682  pntrmax  25832  qabvexp  25894  ostth2lem2  25902  ax5seglem4  26411  axeuclidlem  26441  uhgredgrnv  26608  usgredg4  26692  nbuhgr2vtx1edgblem  26826  vtxduhgr0e  26953  vtxduhgr0nedg  26967  rusgrpropnb  27058  uspgr2wlkeqi  27122  redwlklem  27149  lfgrwlkprop  27165  2pthnloop  27210  spthonepeq  27231  pthdlem2lem  27246  crctcshwlkn0lem3  27288  crctcshwlkn0lem5  27290  crctcshwlkn0lem7  27292  crctcshwlkn0  27297  wlkiswwlks1  27343  wlkiswwlks2  27351  wlkiswwlksupgr2  27353  wwlksnext  27371  wwlksnextproplem2  27401  wwlksnextproplem2OLD  27402  wspthsnonn0vne  27413  2pthon3v  27439  rusgrnumwwlk  27472  erclwwlkeqlen  27524  erclwwlksym  27526  erclwwlktr  27527  erclwwlkneqlen  27582  erclwwlknsym  27584  erclwwlkntr  27585  uhgr3cyclex  27701  upgreupthseg  27728  eupth2lem3lem4  27751  eucrctshift  27763  4cycl2vnunb  27814  nvs  28207  nvtri  28214  nmlno0  28339  nmlnoubi  28340  ubth  28418  hlipgt0  28459  ocnel  28846  elspansn2  29115  elspansn3  29120  normcan  29124  pjoml2  29159  lecm  29165  osum  29193  nmbdfnlb  29598  leopmul  29682  hstpyth  29777  cvnbtwn  29834  ssmd1  29859  ssmd2  29860  ssdmd1  29861  ssdmd2  29862  cvmd  29884  cvdmd  29885  superpos  29902  disji2f  30083  disjif  30084  disjif2  30087  padct  30196  ffs2  30205  bcm1n  30256  omndadd  30403  ogrpaddlt  30415  archiabl  30449  slmdlema  30453  lbslsat  30599  eulerpartlemb  31228  sgn3da  31402  cvmsdisj  32062  cvmlift2lem12  32106  poseq  32556  frrlem12  32595  nosepon  32633  nolesgn2o  32639  nosepnelem  32645  nosepne  32646  nosepdmlem  32648  nosepdm  32649  nodenselem8  32656  noresle  32661  noetalem3  32680  sslttr  32729  scutbdaylt  32737  lineintmo  33079  nn0prpwlem  33131  nn0prpw  33132  neibastop2lem  33169  lindsadd  34274  bddiblnc  34351  areacirc  34376  incsequz  34413  mettrifi  34422  ismtybnd  34475  heiborlem1  34479  rngoisocnv  34649  risci  34655  eqvrelqsel  35244  lfl1  35599  lkrlsp2  35632  omlfh3N  35788  cvrnbtwn  35800  cvrnbtwn2  35804  cvrnbtwn4  35808  cvlexch3  35861  cvlexch4N  35862  cvlatexchb1  35863  2llnne2N  35937  atcvrj0  35957  cvrat2  35958  ps-1  36006  3atlem5  36016  islln2a  36046  lplnriaN  36079  lplnribN  36080  llncvrlpln2  36086  lplncvrlvol2  36144  psubatN  36284  pmapglb2N  36300  pmapglb2xN  36301  2llnma1b  36315  paddasslem17  36365  pmod2iN  36378  pmodl42N  36380  hlmod1i  36385  atmod1i1  36386  atmod1i2  36388  llnmod1i2  36389  pclcmpatN  36430  osumcllem8N  36492  pexmidlem3N  36501  pl42lem4N  36511  4atexlem7  36604  ltrnnid  36665  cdlemc4  36723  cdleme32a  36970  cdlemeg46gfre  37061  cdlemf2  37091  cdlemg4c  37141  trlcoat  37252  tendovalco  37294  tendoeq2  37303  cdlemk36  37442  diael  37572  diatrl  37573  dicelval1stN  37717  dicelval2nd  37718  dihlspsnat  37862  dochkr1  38007  lcfrlem9  38079  mapdh8e  38313  hdmapval0  38362  hgmapval0  38421  nn0rppwr  38559  nn0expgcd  38561  incssnn0  38648  pell14qrexpcl  38805  pell14qrgap  38813  congadd  38904  acongsym  38914  acongtr  38916  dvdsacongtr  38922  jm2.19lem3  38929  jm2.19lem4  38930  jm2.26lem3  38939  relexpiidm  39357  bi13impia  40185  3impcombi  40514  ioogtlb  41147  iocgtlb  41154  iocleub  41155  icoltub  41161  iooltub  41163  limclner  41309  limsupre3lem  41390  climuzlem  41401  elfzelfzlble  42873  subsubelfzo0  42878  iccpartigtl  42901  sqrtpwpw2p  43008  fmtnoprmfac1lem  43034  fmtno4prmfac  43042  evenltle  43190  even3prm2  43192  wtgoldbnnsum4prm  43275  bgoldbnnsum3prm  43277  bgoldbtbndlem1  43278  bgoldbtbndlem3  43280  bgoldbtbndlem4  43281  bgoldbtbnd  43282  upgrwlkupwlk  43323  c0snmgmhm  43489  funcringcsetcALTV2lem9  43619  funcringcsetclem9ALTV  43642  lincscmcl  43794  lindslinindimp2lem4  43823  lincresunit2  43840  lincresunit3  43843  elfzolborelfzop1  43882  m1modmmod  43889  rege1logbzge0  43927  fllog2  43936  dignn0ldlem  43970  rrx2pnecoorneor  44010  rrx2plord2  44017  rrx2linest  44037